$\forall$$A$, $B$:Type$_{\mbox{\scriptsize i}}$, $a$:EqDecider($A$), $b$:EqDecider($B$).
\\[0ex]prod{-}deq{-}aux\{v:l, i:l\}($A$; $B$; $a$; $b$) $\in$ ($\forall$$p$, $q$:($A$$\times$$B$). $p$ $=$ $q$ $\Leftrightarrow$ proddeq($a$;$b$)($p$,$q$))